;;;============================================================
;;;
;;; Subject: my-logbitp
;;;         
;;;
;;;------------------------------------------------------------
;;;
;;; Jónathan Heras Vicente
;;; Beginning date: 15-05-09
;;; End date: 08-09-09
;;;
;;;============================================================

#| Certification code:

(certify-book "my-logbitp" 0 nil)

|#

(in-package "ACL2")

(include-book "dg-binary")

(include-book "my-member-lemmas")

(set-verify-guards-eagerness 0)


;;;****************************************************************
;;;
;;; my-logbitp and properties with my-member
;;;
;;;****************************************************************

(defun my-logbitp (d dgop)
  (declare (xargs :measure (len dgop)))
  (if (natp d)
      (cond ((endp dgop) nil)
	    ((and (eql d 0) (eql (car dgop) 0))  nil)
	    ((and (eql d 0) (eql (car dgop) 1))  t)
	    (t (my-logbitp (- d 1) (cdr dgop))))
  nil))




(defthm my-member-implies-my-member-1+ls
  (implies (and (natp d)
		(dgl-p dgop)
		(my-member (- d 1) dgop)
		)
	   (my-member d (1+ls dgop))))


(defthm not-my-member-implies-not-my-member-1+ls
  (implies (and (natp d)
		(dgl-p dgop)
		(not (my-member (- d 1) dgop))
		)
	   (not (my-member d (1+ls dgop)))))

(defthm my-member-implies-my-member-append
  (implies (and (natp d)
		(dgl-p dgop)
		(my-member d dgop)
		)
	   (my-member d (append dgop (list 0)))))


(defthm my-member-implies-my-member-append-1+ls
  (implies (and (natp d)
		(dgl-p dgop)
		(my-member (- d 1) dgop)
		)
	   (my-member d (append (1+ls dgop) (list 0)))))

(defthm not-my-member-implies-not-my-member-append-1+ls
  (implies (and (natp d)
		(dgl-p dgop)
		(consp dgop)
		(not (my-member (- d 1) dgop))
		(not (equal d 0))
		(not (equal (+ -1 d) 0)))
	   (not(my-member d (append (1+ls dgop) (list 0))))))


(defthm my-member-implies-my-member-append-d=1
  (implies (and (natp d)
		(equal (+ -1 d) 0)
		(dgl-p dgop)		
		)
	   (my-member d (append dgop (list 0)))))


(defthm my-logbitp-cdr-implies-my-logbitp
  (implies (and (natp d)
		(dgb-p dgop)
		(my-logbitp (- d 1) (cdr dgop))
		)
	   (my-logbitp d dgop))
:hints (("Goal" :induct (my-logbitp d dgop)))
)

(defthm not-my-logbitp-cdr-my-logbit-implies-d=0
  (implies (and (natp d)
		(dgb-p dgop)
		(not (my-logbitp (- d 1) (cdr dgop)))
		(my-logbitp d dgop)
		)
	   (eql d 0))
:rule-classes nil
)

(defthm append-my-member
  (implies (and (eql d 0)
		(dgl-p dgl)
		)
	   (my-member d (append dgl (list 0)))))


(defthm my-logbitp-implies-my-member-help*1/10-aux1
  (implies (and (natp d)
		(dgb-p dgop)
		(not (my-logbitp (- d 1) (cdr dgop)))
		(my-logbitp d dgop)
		(not (eql (car dgb) 0))
		)
	   (equal (dgb->dgl dgop)
		  (append (1+ls (dgb->dgl (cdr dgop))) (list 0)))))
	   


(defthm 1+ls-dgb
  (implies (dgl-p dgl)
	   (dgl-p (1+ls dgl))))

(defthm my-logbitp-implies-my-member-help*1/10
  (implies (and (natp d)
		(dgb-p dgop)
		(not (my-logbitp (- d 1) (cdr dgop)))
		(my-logbitp d dgop)
		(not (eql (car dgb) 0))
		)
	   (my-member d (dgb->dgl dgop))
	   )
:hints (("Goal" :do-not-induct t
	 :use ((:instance my-logbitp-implies-my-member-help*1/10-aux1)
	       (:instance not-my-logbitp-cdr-my-logbit-implies-d=0)
	       (:instance append-my-member
			  (d d) (dgl (1+ls (dgb->dgl (cdr dgb))))))
	 ))
)
   

(defthm my-logbitp-implies-my-member 
  (implies (and (natp d)
		(dgb-p dgb)
		(my-logbitp d dgb))
	   (my-member d (dgb->dgl dgb))))


(defthm my-logbitp-implies-cmp-d-ls-d-do 
  (implies (and (natp d)
		(dgb-p dgb)
		(my-logbitp d dgb))
	   (null (cmp-d-ls-d-do d (dgb->dgl dgb))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance my-logbitp-implies-my-member)
	       (:instance my-member-implies-face-do-null
			  (i d) (ls (dgb->dgl dgb)))))))


(defun my-logbitp-implies-my-member-d-1-schema (d dgb)
  (declare (xargs :measure (len dgb)))
  (if (or (not (plusp d)) (not (dgb-p dgb)) 
	  (not (my-logbitp (- d 1) dgb))
	  )
      nil
    (if (endp dgb)
	t
      (my-logbitp-implies-my-member-d-1-schema (- d 1) (cdr dgb)))
))
 

(defthm my-logbitp-implies-my-member-d-1 
  (implies (and (plusp d)
		(dgb-p dgb)
		(my-logbitp (- d 1) dgb))
	   (my-member d (dgb->dgl dgb)))
:hints (("Goal" :induct 
	 (my-logbitp-implies-my-member-d-1-schema d dgb))
	("Subgoal *1/2.6" :do-not-induct t
	 :use ((:instance my-member-implies-my-member-1+ls
			  (d d) (dgop (dgb->dgl (cdr dgb))))))
	("Subgoal *1/2.5" :do-not-induct t
	 :use ((:instance my-member-implies-my-member-append-d=1 
			  (d d) (dgop (1+ls (dgb->dgl (cdr dgb)))))))
	("Subgoal *1/2.3" :do-not-induct t
	 :use ((:instance  my-member-implies-my-member-append-1+ls
			  (d d) (dgop (dgb->dgl (cdr dgb))))))))



(defthm my-logbitp-d-1-implies-cmp-d-ls-d-do 
  (implies (and (natp d)
		(dgb-p dgb)
		(my-logbitp (- d 1) dgb))
	   (null (cmp-d-ls-d-do d (dgb->dgl dgb))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance my-logbitp-implies-my-member-d-1)
	       (:instance my-member-implies-face-do-null
			  (i d) (ls (dgb->dgl dgb)))))))



(defthm not-my-member-0-dgop-1+ls
  (implies (and (< (+ -1 d) 0)
		(natp d)
		(dgl-p dgop))
	   (not (my-member d (1+ls dgop)))))
		

(defthm not-my-logbitp-not-my-logbitp-d-1-implies-not-my-member 
  (implies (and (natp d)
		(dgb-p dgb)
		(not (my-logbitp d dgb))
		(not (my-logbitp (- d 1) dgb)))		
	   (not (my-member d (dgb->dgl dgb))))
:hints (("Subgoal *1/13.2" :do-not-induct t
	 :use ((:instance not-my-member-implies-not-my-member-append-1+ls
			  (d d) (dgop (dgb->dgl (cdr dgb))))
	       ))))


(defthm not-my-logbitp-not-my-logbitp-d-1-implies-cmp-d-ls-d-do
  (implies (and (natp d)
		(dgb-p dgb)
		(not (my-logbitp d dgb))
		(not (my-logbitp (- d 1) dgb)))
	   (cmp-d-ls-d-do d (dgb->dgl dgb)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-my-logbitp-not-my-logbitp-d-1-implies-not-my-member)
	       (:instance not-my-member-implies-face-do-not-null
			  (i d) (ls (dgb->dgl dgb)))))))


;;;****************************************************************
;;;
;;; (implies (1dlop-dgop-binary-do d dgop)
;;;	   (null (cmp-d-ls-d-do d (dgb->dgl dgop)))
;;;		  )
;;;
;;;****************************************************************

(defun 1dlop-dgop-binary-do (d dgop)
  (or (my-logbitp d dgop)
      (my-logbitp (- d 1) dgop))
  )


(defthm 1dlop-dgop-binary-do-implies-null-cmp-d-ls-d-do
  (implies (and (natp d)
		(dgb-p dgb)
		(1dlop-dgop-binary-do d dgb))
	   (null (cmp-d-ls-d-do d (dgb->dgl dgb))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance my-logbitp-implies-cmp-d-ls-d-do)
	       (:instance my-logbitp-d-1-implies-cmp-d-ls-d-do)))))


(defthm null-1dlop-dgop-binary-do-implies-cmp-d-ls-d-do
  (implies (and (natp d)
		(dgb-p dgb)
		(null (1dlop-dgop-binary-do d dgb)))
	   (cmp-d-ls-d-do d (dgb->dgl dgb)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance not-my-logbitp-not-my-logbitp-d-1-implies-cmp-d-ls-d-do)
	       ))))

  
